This invention relates generally to analysis of circuit designs, and more particularly to analyzing the behavior of sets of trace signatures.
As the complexity in circuit design has increased, there has been a corresponding need for improvements in various kinds of analysis and debugging techniques. In fact, these analysis and debugging techniques have evolved from relatively simple transistor circuit-level simulation (in the early 1970s) to logic gate-level simulation (in the late 1980s) to the current art that uses Register Transfer Language (RTL)-level simulation, and formal verification. RTL describes the registers of a computer or digital electronic system and the way in which data are transferred among the combinational logic between registers.
Existing verification and debugging tools are used in the design flow of a circuit. The design flow begins with the creation of a circuit design at the RTL level using RTL source code. The RTL source code is specified according to a Hardware Description Language (HDL), such as Verilog HDL or VHDL. Circuit designers use high-level hardware description languages because of the size and complexity of modern integrated circuits. Circuit designs are developed in a high-level language using computer-implemented software applications, which enable a user to use text-editing and graphical tools to create a HDL-based design.
An increasingly popular technique is to use formal methods to verify the properties of a design completely. Formal methods use mathematical techniques to prove that a design property is either always true or to provide an example condition (called a counterexample) that demonstrates the property is false. Many tools that use formal methods to verify RTL source code and design properties are known as “model checkers.” Design properties to be verified include specifications and/or requirements that must be satisfied by the circuit design. The formal verification technology requires that the requirements are expressed in a formal notation, for example a temporal language (such as PSL and SVA), which enables an exhaustive mathematical check whether a design complies with the requirements.
An existing method of analysis explores the RTL level in view of a multi-bit signal. The method explores different ways to exercise a circuit design resulting in varying the value of the multi-bit signal. Similarly, different ways of exercising a circuit design resulting in a consistent value for the multi-bit signal may be explored. In one instance, an initial trace is received and an expression is obtained describing the value of a target multi-bit signal. The expression is negated and used as a constraint in generating an additional trace which serves as an extension to the initial trace. This process is repeated to generate additional trace extensions, but it is unclear to the user what commonalities and differences are present in the various segments of the resulting trace. Each additional trace is generated by appending additional signal values to the end of its parent trace.